Issue5434-1.agda:4,3-4
(@0 A : Set) → D A is not usable at the required modality
when checking that the type (@0 A : Set) → D A of the constructor c
fits in the sort Set₁ of the datatype.
